cond\_rel\_implies($T$;$P$;$R_{1}$;$R_{2}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$x$:$T$, $y$:$T$. $P$($x$) $\Rightarrow$ ($x$ $R_{1}$ $y$) $\Rightarrow$ ($x$ $R_{2}$ $y$)